Inference at * 1 1 
Iof proof for Lemma ifthenelse wf:



1. b : ?Unit
2. A : Type
3. p : A
4. q : A
  case b of inl() => p | inr() => q  A 

latex

 by ((((D 1) 
CollapseTHEN (Reduce 0))) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n
C),(first_nat 4:n)) (first_tok :t) inil_term))) 

latex

C.

Definitions

t  T